l, l2:IdLnk, dt:tg:Id fp Type, tg:Id. rcv(l2,tg)  dom(lnk-decl(l;dt))  l2 = l 

latex

Definitions	P & Q, t  T, {T}, P  Q, x:A. B(x), x:A. B(x), IdLnk, Id, rcv(l,tg), Knd, P  Q, map(f;as), KindDeq, b, x  dom(f), lnk-decl(l;dt), a:A fp B(a), x. t(x), Top
Lemmas	assert wf, fpf-dom wf, fpf-trivial-subtype-top, lnk-decl wf, fpf wf, IdLnk wf, assert-deq-member, Kind-deq wf, map wf, member map, Knd wf, rcv wf, Id wf, rcv one one